Inference at * 2 1 1 2 1 
Iof proof for Lemma before-adjacent:



1. T : Type
2. T List
3. u : T
4. v : T List
5. x, y:T.
5. no_repeats(T;v)  adjacent(T;v;x;y)  (z:T. z before y  v  (z before x  v  (z = x)))
6. x : T
7. y : T
8. no_repeats(T;v)
9. (u  v)
10. 0 < ||v||
11. x = u
12. y = hd(v)
13. z : T
14. z before y  v
  ((z = u & (x  v))  z before x  v)  (z = x) 

latex

 by ((InstLemma `hd-before` [T;v;z]) 
CollapseTHEN (Auto)) 

latex

C1: .....antecedent..... NILNIL

C1:   (z  v)
C2: .....antecedent..... NILNIL

C2:   (z = hd(v))
C3: 

C3: 15. hd(v) before z  v
C3:   ((z = u & (x  v))  z before x  v)  (z = x)
C.

Definitions	t  T, hd(l), False, P  Q, Void, a < b, A, no_repeats(T;l), type List, Type, P & Q, x:A  B(x), (x  l), x before y  l, s = t, ||as||, x:A. B(x), x:AB(x), P  Q, left + right
Lemmas	hd-before, l member wf, l before wf